(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v9 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const _25-0 (_ BitVec 25))
(assert (and v9 v0 v13 (= (_ bv273 9) (_ bv273 9) (_ bv273 9) (_ bv273 9)) v6 v1 v7 (distinct _25-0 (bvadd _25-0 _25-0))))
(check-sat)
